#include <vector>
#include <string>
#include <iostream>
#include <fstream>
#include <queue>
#include <goto_functions.h>
#include <cmdline.h>
#include "cfa_impl.h"
#include <ansi_c_language.h>
#include <language_ui.h>
#include <options.h>
#include <config.h>
#include <goto_convert_functions.h>
#include <mode.h>
using namespace std;

//extern vector<Prog*> fun;
//extern Prog* prog1;
std::vector<NotMidterm> not_replace;
//std::map<Node*, Node*> not_replace;

std::map<std::string, std::map<std::string, std::string> > struct_info;
std::map<std::string, std::map<std::string, int> > enum_info;


bool isBadNode(Node* n){
        return typeid(*n) == typeid(BadNode);
}
bool isBinNode(Node* n){
        return typeid(*n) == typeid(BinNode);
}
Node* getTNode(Node* n){
	return ((BinNode*)n)->_true;
}
Node* getFNode(Node* n){
	return ((BinNode*)n)->_false;
}
Prop* getProp(Node* n){
	return ((BinNode*)n)->p;
}
bool isAssignNode(Node* n){
	return (typeid(*n) ==typeid(UniNode))&&(((UniNode*)n)->st==st_Assign);
}
VarExpr* getLval(Node* n){
	return ((VarExpr*)((UniNode*)n)->e1);
}
Expr* getRval(Node* n){
	return ((UniNode*)n)->e2;
}
Node* getNext(Node* n){
	return ((UniNode*)n)->next;
}
bool isCallNode(Node* n){
	return (typeid(*n) ==typeid(UniNode))&&(((UniNode*)n)->st==st_FUNC_Call);
}
void PrintPropType(PropType l){
    if(l == LT){ cout << "<"; }
    else if(l == GT){ cout << ">"; }
    else if(l == Eq){ cout << "=="; }
    else{ }
}
vector<Expr*> getActPara(Node* n){
	return ((UniNode*)n)->actualpara;
}
char* getFunName(Node* n){
	Expr *e=((UniNode*)n)->e2;
	assert(typeid(*e) == typeid(VarExpr));
        return ((VarExpr*)e)->x;
}
bool isReturnNode(Node* n){
	return (typeid(*n) ==typeid(UniNode))&&(((UniNode*)n)->st==st_Return);
}
Expr* getRetExpr(Node* n){
	return ((UniNode*)n)->e1;
}

void getCFA(vector<CFA*> &result, vector<Expr*> &vv,int argc, const char **argv) {
	vector<CFA_impl> vnewCFA;
	cmdlinet cmdline;
	goto_functionst goto_functions;
	cmdline.parse(argc, argv,"");

	language_uit lang("parse", cmdline);
	register_language(new_ansi_c_language);
	config.set(cmdline);

	lang.parse();
	lang.typecheck();
	lang.final();
	lang.clear_parse();

	goto_convert(lang.context, optionst(), goto_functions, lang.ui_message_handler);

	namespacet ns(lang.context);
	goto_functions.output(vnewCFA, ns, std::cout);
	vnewCFA.erase(vnewCFA.begin(), vnewCFA.begin()+2);

	for(int i1 = 0; i1 < (int)vnewCFA.size(); i1++){
		if(strcmp(vnewCFA[i1].GetId(), "__CPROVER_initialize") == 0){
			vnewCFA[i1].GetGlobalVariable(vv);
		}
		result.push_back(&vnewCFA[i1]);
	}
}


bool UniNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(UniNode)){
        if(((UniNode*)t)->e1 == ((UniNode*)this)->e1 && \
           ((UniNode*)t)->e2 == ((UniNode*)this)->e2 ){
            return true;
        }
        else{
            return false;
        }
    }
    else{
        return false;
    }
}
bool BinNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(BinNode)){
        if(((BinNode*)t)->p == ((BinNode*)this)->p){
            return true;
        }
        else{
            return false;
        }
    }
    else{
        return false;
    }
}
bool BadNode::operator==(Node &other){
    Node* t = &other;
    if(typeid(*t) == typeid(BadNode)){
        return true;
    }
    else{
        return false;
    }
}

InequProp* CFA_impl::AssignExpr2Prop(Expr* e1, Expr* e2){
    InequProp* p1 = new InequProp;
    p1->e1 = e1;
    p1->e2 = e2;
    p1->p = Eq;
    return p1;
}
void CFA_impl::ConnectGoto(map<Node*, char*>* gotolist){
    int i1, Flag;
    Node *bn;
    queue<Node*> visited, unvisited;
    map<Node*, char*>::iterator it;
    map<Node*, char*>::iterator label_it;
    for(it = gotolist->begin(); it != gotolist->end(); it++){
        //初始化
        Flag = 0;
        while(!visited.empty()){ visited.pop(); }
        while(!unvisited.empty()){ unvisited.pop(); }
        if(strcmp(it->second, "break") == 0){
            //BFS
            unvisited.push(it->first);
	    while(!unvisited.empty()){
                bn = (unvisited.front());
                for(i1 = 0; i1 < (int)bn->prev.size(); i1++){
                    unvisited.push(bn->prev[i1]);
                }
                for(i1 = 0; i1 < (int)LoopStart.size(); i1++){
                    if(LoopStart[i1] == bn){
                        Flag = 1;
                        ((UniNode*)it->first)->next = *LoopEnd[i1];
                        cout << "break = " << *LoopEnd[i1] << endl;
                        break;
                    }
                }
                if(Flag == 1){
                    break;
                }
                visited.push(bn);
                unvisited.pop();
            }
        }
        else if(strcmp(it->second, "continue") == 0){
            //BFS
            unvisited.push(it->first);
	    while(!unvisited.empty()){
                bn = (unvisited.front());
                for(i1 = 0; i1 < (int)bn->prev.size(); i1++){
                    unvisited.push(bn->prev[i1]);
                }
                for(i1 = 0; i1 < (int)LoopStart.size(); i1++){
                    if(LoopStart[i1] == bn){
                        Flag = 1;
                        ((UniNode*)it->first)->next = LoopStart[i1];
                        break;
                    }
                }
                if(Flag == 1){
                    break;
                }
                visited.push(bn);
                unvisited.pop();
            }
        }
        else{
            for(label_it=LabelSet.begin(); label_it != LabelSet.end(); label_it++){
                if(strcmp(label_it->second, it->second) == 0){
                    ((UniNode*)(it->first))->next =label_it->first;
                }
            }
        }
    }
}
int exp(int x, int t){
    int i1, i2;
    i2 = 1;
    for(i1 = 0; i1 < t; i1++){
        i2 = i2 * x;
    }
    return i2;
}
string Int2String(int y){
    string r;
    r.clear();
    int i1, i2, x, z;
    if(y == 0){ return "0"; }
    z = y;
    if(y < 0){ x = (-1)*y; y = (-1)*y; }
    else{ x = y; }
    for(i1 = 0; y > 0; y=y/10){
        i1 = i1 + 1;
    }
    for(; i1 > 0; i1--){
        i2 = x / exp(10, i1-1);
        x = x % exp(10, i1-1);
        r = r + (char)(i2+48);
    }
    if(z < 0){  r = "-" + r; }
    return r;
}
string OPType2String(OPType l){
    string s;
    if(l == Plus){ return "+"; }
    else if(l == Minus){ return "-"; }
    else if(l == Multi){ return "*"; }
    else if(l == Divide){ return "/"; }
/*    else if(l == Bitor){ return "|"; }
    else if(l == Bitand){ return "&"; }
    else if(l == Bitxor){ return "^"; }
    else if(l == Mod){ return "mod"; }*/
    else return "";
}

string Expr2String(Expr* e){
    string s;
    if(typeid(*e) == typeid(IntExpr)){
        s = Int2String(((IntExpr*)e)->i);
    }
/*    else if(typeid(*e) == typeid(SelectExpr)){
        s = Expr2String(((SelectExpr*)e)->a);
        s = s + "[";
        s = s + Expr2String(e);
        s = s + "]";
    }*/
    else if(typeid(*e) == typeid(VarExpr)){
        s = ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        s = Expr2String(((BinExpr*)e)->e1);
        s = s + OPType2String(((BinExpr*)e)->op);
        s = s + Expr2String(((BinExpr*)e)->e2);
    }
    else{
        cout << "error" << endl;
    }
    return s;
}
string LogicType2String(LogicType l){
    if(l == And){ return "&&"; }
    else { return "||"; }
}
string PropType2String(PropType l){
    if(l == LT){ return "<"; }
    else if(l == GT){ return ">"; }
    else { return "=="; }
}


string Prop2String(Prop* p){
    string result;
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ result = "TRUE"; }
        else if(((BoolProp*)p)->b == false){ result = "FALURE"; }
        else{ cout << "error"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        cout << "~ ";
        result = Prop2String(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        result = Prop2String(((BinProp*)p)->p1);
        result = result + LogicType2String(((BinProp*)p)->l);
        result = result + Prop2String(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        result = Expr2String(((InequProp*)p)->e1);
        result = result + PropType2String(((InequProp*)p)->p);
        result = result + Expr2String(((InequProp*)p)->e2);
    }
    else{
        cout << "error" << endl;
    }
    return result;
}

void CFA_impl::SetUniNodeStatement(Node* n, int type, char *s){//type 1: assign, type 2: goto, type 3: return, type4: label, type5 funtion call
    int i1;
    char state[256];
    if(typeid(*n) == typeid(UniNode)){
        if(type == 1){
            strcpy(state, ((VarExpr*)(((UniNode*)n)->e1))->x);
            strcat(state, "=");
            strcat(state, (Expr2String(((UniNode*)n)->e2)).c_str());
        }
        else if(type == 2){
            strcpy(state, "goto ");
            strcat(state, s);
        }
        else if(type == 3){
            strcpy(state, s);
            strcat(state, " ");
            strcat(state, (Expr2String(((UniNode*)n)->e1)).c_str());
        }
        else if(type == 4){
            strcpy(state, s);
            strcat(state, ":");
        }
        else if(type == 5){
            strcpy(state, s);
            strcat(state, "(");
            for(i1 = 0; i1 < (int)((((UniNode*)n)->actualpara).size()); i1++){
                strcat(state, (Expr2String(((UniNode*)n)->actualpara[i1])).c_str());
                if(i1 != (int)((((UniNode*)n)->actualpara).size())-1){
                    strcat(state, ", ");
                }
            }
            strcat(state, ");");
        }
        else{
            cout << "error1" << endl;
        }
        strcpy(((UniNode*)n)->statement, state);
    }
    else{
        cout << "error2" << endl;
    }
}

/*
ProgramConnectType CFA_impl::BuildCFA(Prog prog, Node* m, Node *Term, map<Node*, char*> *gotolist){
    int i1, i2;
    i1 = 0; i2 = 0;
    Node *n = NULL;
    //InequProp *p1 = NULL;
    ProgramConnectType pct, pct1, pct2;
    vector<Node**> nodeptr1;
    vector<Node*> nodeptr2;
    //cout << "statment.size = " << prog.p.size() << endl;
    for(i1 = 0; i1 < (int)(prog.p.size()); i1++){
        cout << "prog.size = " << prog.p.size() << " i1 = " << i1;
        if(typeid(*prog.p[i1]) ==  typeid(AssignStmt)){ //assign statment
            cout << " type = Assign" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Assign;
        }
        else if(typeid(*prog.p[i1]) == typeid(AssertStmt)){ // assert statement
            cout << " type = Assert" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(IfStmt)){ // if statment
            cout << " type = If" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(WhileStmt)){ // while statment
            cout << " type = While" << endl;
            n = new BinNode;
        }
        else if(typeid(*prog.p[i1]) == typeid(GotoStmt)){ // goto statment
            cout << " type = Goto" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Goto;
        }
        else if(typeid(*prog.p[i1]) == typeid(LabelStmt)){ // goto statment
            cout << " type = Label" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_Label;
        }
        else if(typeid(*prog.p[i1]) == typeid(CallFunStmt)){ // goto statment
            cout << " type = CallFun" << endl;
            n = new UniNode;
            ((UniNode*)n)->st=st_FUNC_Call;
        }
        else{
        }
        if(i1 == 0){ 
            pct.init = n;
        }
        else{
            for(i2 = 0; i2 < (int)nodeptr1.size(); i2++){
                (*nodeptr1[i2]) = n;
            }
            nodeptr1.clear();
            for(i2 = 0; i2 < (int)nodeptr2.size(); i2++){
                n->prev.push_back(nodeptr2[i2]);
            }
            nodeptr2.clear();
        }
        if(typeid(*prog.p[i1]) ==  typeid(AssignStmt)){ //assign statment
            //p1 = AssignExpr2Prop(((AssignStmt*)prog.p[i1])->e1,((AssignStmt*)prog.p[i1])->e2);
            //((UniNode*)n)->p = p1;
            ((UniNode*)n)->e1 = ((AssignStmt*)prog.p[i1])->e1;
            ((UniNode*)n)->e2 = ((AssignStmt*)prog.p[i1])->e2;
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
            SetUniNodeStatement(n, 1, NULL);
        }
        else if(typeid(*prog.p[i1]) == typeid(AssertStmt)){ // assert statement
            ((BinNode*)n)->p = ((AssertStmt*)prog.p[i1])->p;
            nodeptr1.push_back(&(((BinNode*)n)->_true));
            nodeptr2.push_back(n);
            ((BinNode*)n)->_false = m;
        }
        else if(typeid(*prog.p[i1]) == typeid(IfStmt)){ // if statment
            ((BinNode*)n)->p = ((IfStmt*)prog.p[i1])->p;
            if(((IfStmt*)prog.p[i1])->p1 != NULL){
                pct1 = BuildCFA(*(((IfStmt*)prog.p[i1])->p1), m, Term, gotolist);
                ((BinNode*)n)->_true = ((pct1.init));
                pct1.init->prev.push_back(n);
                for(i2 = 0; i2 < (int)pct1.ends1.size(); i2++){
                    nodeptr1.push_back(pct1.ends1[i2]);
                }
                for(i2 = 0; i2 < (int)pct1.ends2.size(); i2++){
                    nodeptr2.push_back(pct1.ends2[i2]);
                }
            }
            if(((IfStmt*)prog.p[i1])->p2 != NULL){
                pct2 = BuildCFA(*(((IfStmt*)prog.p[i1])->p2), m, Term, gotolist);
                ((BinNode*)n)->_false = ((pct2.init));
                pct2.init->prev.push_back(n);
                for(i2 = 0; i2 < (int)pct2.ends1.size(); i2++){
                    nodeptr1.push_back(pct2.ends1[i2]);
                }
                for(i2 = 0; i2 < (int)pct2.ends2.size(); i2++){
                    nodeptr2.push_back(pct2.ends2[i2]);
                }
            }
            else{
                //
                nodeptr1.push_back(&(((BinNode*)n)->_false));
                nodeptr2.push_back(n);
            }
        }
        else if(typeid(*prog.p[i1]) == typeid(WhileStmt)){ // while statment
            ((BinNode*)n)->p = (((WhileStmt*)prog.p[i1])->p);
            pct1 = BuildCFA(*(((IfStmt*)prog.p[i1])->p1), m, Term, gotolist);
            ((BinNode*)n)->_true = (pct1.init);
            pct1.init->prev.push_back(n);
            nodeptr1.push_back(&(((BinNode*)n)->_false));
            for(i2 = 0; i2 < (int)pct1.ends1.size(); i2++){
                *(pct1.ends1[i2]) = n;
            }
            nodeptr2.push_back(n);
            LoopStart.push_back(n);
            LoopEnd.push_back(&(((BinNode*)n)->_false));
        }
        else if(typeid(*prog.p[i1]) == typeid(GotoStmt)){ // Goto statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            //nodeptr1.push_back(&(((UniNode*)n)->next));// this is not right
            if(strcmp(((GotoStmt*)prog.p[i1])->L, "continue") != 0 && strcmp(((GotoStmt*)prog.p[i1])->L,"break") != 0 && strcmp(((GotoStmt*)prog.p[i1])->L,"return") != 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                //strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                SetUniNodeStatement(n, 2, ((GotoStmt*)(prog.p[i1]))->L);
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "continue") == 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                //SetUniNodeStatement(n, 3, "continue");
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "break") == 0){
                gotolist->insert(pair<Node*, char*>(n, ((GotoStmt*)prog.p[i1])->L));
                strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                //SetUniNodeStatement(n, 3, "break");
            }
            else if(strcmp(((GotoStmt*)prog.p[i1])->L, "return") == 0){
                ((UniNode*)n)->next = Term;
                //strcpy(((UniNode*)n)->statement, ((GotoStmt*)(prog.p[i1]))->L);
                ((UniNode*)n)->e1 = ((GotoStmt*)(prog.p[i1]))->e;
                SetUniNodeStatement(n, 3, ((GotoStmt*)prog.p[i1])->L);
            }
            else{
            }
            nodeptr2.push_back(n);
        }
        else if(typeid(*prog.p[i1]) == typeid(LabelStmt)){ // Label statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            LabelSet.insert( pair<Node*, char*>(n, ((LabelStmt*)(prog.p[i1]))->L) );
            //strcpy(((UniNode*)n)->statement, ((LabelStmt*)(prog.p[i1]))->L);
            SetUniNodeStatement(n, 4, ((LabelStmt*)(prog.p[i1]))->L);
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
        }
        else if(typeid(*prog.p[i1]) == typeid(CallFunStmt)){ // Label statment
            ((UniNode*)n)->e1 = NULL;
            ((UniNode*)n)->e2 = NULL;
            strcpy(((UniNode*)n)->name, ((CallFunStmt*)(prog.p[i1]))->fun);
            ((UniNode*)n)->actualpara = ((CallFunStmt*)(prog.p[i1]))->para;
            SetUniNodeStatement(n, 5, ((CallFunStmt*)(prog.p[i1]))->fun);
            nodeptr1.push_back(&(((UniNode*)n)->next));
            nodeptr2.push_back(n);
        }
        else{
        }
    }
    pct.ends1 = nodeptr1;
    pct.ends2 = nodeptr2;
    return pct;
}
*/
void PrintLogicType(LogicType l){
    if(l == And){ cout << "&&"; }
    else if(l == Or){ cout << "||"; }
    else{ }
}
void PrintProp(Prop* p){
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ cout << "TRUE"; }
        else if(((BoolProp*)p)->b == false){ cout << "TRUE"; }
        else{ cout << "error"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        cout << "~ ";
        PrintProp(((NegProp*)p)->p);
    }
    else if(typeid(*p) == typeid(BinProp)){
        PrintProp(((BinProp*)p)->p1);
        PrintLogicType(((BinProp*)p)->l);
        PrintProp(((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        PrintExpr(((InequProp*)p)->e1);
        PrintPropType(((InequProp*)p)->p);
        PrintExpr(((InequProp*)p)->e2);
    }
    else{
        cout << "error" << endl;
    }
}
void PrintOPType(OPType l){
    if(l == Plus){ cout << "+"; }
    else if(l == Minus){ cout << "-"; }
    else if(l == Multi){ cout << "*"; }
    else if(l == Divide){ cout << "/"; }
/*    else if(l == Bitor){ cout << "|"; }
    else if(l == Bitand){ cout << "&"; }
    else if(l == Bitxor){ cout << "^"; }
    else if(l == Mod){ cout << "mod"; }*/
    else{ }
}
void PrintExpr(Expr* e){
    if(e == NULL){ return; }
    else if(typeid(*e) == typeid(IntExpr)){
        cout << ((IntExpr*)e)->i;
    }
/*    else if(typeid(*e) == typeid(SelectExpr)){
        cout << Expr2String(((SelectExpr*)e)->a) << "[";
        PrintExpr(e);
        cout << "]";
    }*/
    else if(typeid(*e) == typeid(VarExpr)){
        cout << ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        PrintExpr(((BinExpr*)e)->e1);
        PrintOPType(((BinExpr*)e)->op);
        PrintExpr(((BinExpr*)e)->e2);
    }
    else{
        cout << "error" << endl;
    }
    //cout << e << endl;
}
void PrintNode(Node* n){
    //cout << "n = " << n << endl;
    cout << "============================ " << endl;
    if(n == NULL){
        cout << "terminalNode" << endl;
    }
    else if(typeid(*n) == typeid(UniNode)){
        cout << "Node: " << n << endl;
        cout << "Next: " << ((UniNode*)n)->next << endl;
        cout << "Type: UniNode!!! " << endl << " op:"; 
        //PrintProp(((UniNode*)n)->p);
        if(((UniNode*)n)->e1 == NULL && ((UniNode*)n)->e2 == NULL){
            if(((UniNode*)n)->st == st_Return){ cout << "Return"; }
            else{
                cout << ((UniNode*)n)->statement << endl;
            }
        }
        else if(((UniNode*)n)->e1 != NULL &&((UniNode*)n)->e2 == NULL ){
            if(((UniNode*)n)->st == st_Goto){ cout << "Goto "; }
            else if(((UniNode*)n)->st == st_Label){ cout << "Label "; }
            else if(((UniNode*)n)->st == st_Return){ cout << "Return "; }
            else if(((UniNode*)n)->st == st_FUNC_Call){ cout << "Func "; }
            else if(((UniNode*)n)->st == st_None){ cout << "Dummy "; }
            else{ cout << "other"; }
	    PrintExpr(((UniNode*)n)->e1);
        }
        else if(((UniNode*)n)->e1 == NULL){
            if(((UniNode*)n)->st == st_Return){ cout << "Return"; }
            else if(((UniNode*)n)->st == st_FUNC_Call){ 
                cout << "Func "; 
                PrintExpr(((UniNode*)n)->e2);
            }
            else{
                cout << "e1== NULL";
            }
        }
        else{ 
	    PrintExpr(((UniNode*)n)->e1);
            cout << ":=";
            PrintExpr(((UniNode*)n)->e2);
            if(((UniNode*)n)->st == st_FUNC_Call){ 
                cout << "(";
                for(int i1 = 0; i1 < (int)((((UniNode*)n)->actualpara).size()); i1++){
                    PrintExpr((((UniNode*)n)->actualpara)[i1]);
                    if(i1 != (int)((((UniNode*)n)->actualpara).size())-1){
                        cout << ", ";
                    }
                }
                cout << ")";
            }
        }
        //cout <<((UniNode*)n)->GetNext() << endl;
        //printf("%d\n", ((UniNode*)n)->GetNext());
        //PrintProp(((UniNode*)n)->GetNext()->GetP());
        /*if(typeid(*(((UniNode*)n)->next)) == typeid(UniNode) ){
            cout << endl; cout << ", Next = ";
            //PrintProp(((UniNode*)((UniNode*)n)->next)->p);
            PrintExpr(((UniNode*)(((UniNode*)n)->next))->e1);
            cout << "=";
            PrintExpr(((UniNode*)(((UniNode*)n)->next))->e2);
        }
        else if(typeid(*((UniNode*)n)->next) == typeid(BinNode)){
            cout << endl << ", Next1 = ";
            PrintProp(((BinNode*)(((UniNode*)n)->next))->p);
        }
        else{
            cout << endl << ", Next1 = terminal";
        }*/
        //只印內容
        cout << endl;
        cout << "line = " << n->line << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        cout << "Node: " << n << endl;
        cout << "Next: _true: " << ((BinNode*)n)->_true << ", _false:" << ((BinNode*)n)->_false << endl;
        cout << "Type: BinNode!!! " << endl; 
        cout << "op:";
        PrintProp(((BinNode*)n)->p);
        /*if(typeid(*((BinNode*)n)->_true) == typeid(UniNode) ){
            cout << endl << ", Next1 = ";
            //PrintProp(((UniNode*)((BinNode*)n)->_true)->p);
            PrintExpr(((UniNode*)((BinNode*)n)->_true)->e1);
            cout << "=";
            PrintExpr(((UniNode*)((BinNode*)n)->_true)->e2);
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            cout << endl << ", Next1 = ";
            PrintProp(((BinNode*)(((BinNode*)n)->_true))->p);
        }
        else{
            cout << endl << ", Next1 = terminal";
        }
        if(typeid(*((BinNode*)n)->_false) == typeid(UniNode) ){
            cout << endl << ", Next2 = ";
            //PrintProp(((BinNode*)((BinNode*)n)->_false)->p);
            PrintExpr(((UniNode*)((BinNode*)n)->_false)->e1);
            cout << "=";
            PrintExpr(((UniNode*)((BinNode*)n)->_false)->e2);
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            cout << endl << ", Next2 = ";
            PrintProp(((BinNode*)(((BinNode*)n)->_false))->p);
        }
        else if(typeid(*n) == typeid(BadNode)){
            cout << ", Next2 = BadNode" << endl;
        }
        else{
            cout << endl << ", Next2 = terminal";
        }*/
        //只印內容
        cout << endl;
        cout << "line = " << n->line << endl;
    }
    else if(typeid(*n) == typeid(BadNode)){
        cout << "Node: " << n << endl;
        cout << "Type: BadNode" << endl;
        cout << "line = " << n->line << endl;
    }
    else{
    }


}
bool CFA_impl::IsFound(vector<Node*> *visit, Node* X){
    //PrintNode(X);
    int i1;
    bool result;
    i1 = 0; result = false;
    for(i1 = 0; i1 < (int)visit->size(); i1++){
        if((*visit)[i1] == X){ result = true; }
    }
    return result;
}
void CFA_impl::RecursiveVerifyNode(Node* X, set<Node*>& visit){
    if(visit.find(X) != visit.end()){ return; }
    //cout << "X = " << X << endl;
    PrintNode(X);
    visit.insert(X);
    if(X == NULL){ return;   }
    else if(typeid(*X) == typeid(UniNode)){ 
        RecursiveVerifyNode(((UniNode*)X)->next, visit);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveVerifyNode(((BinNode*)X)->_true, visit);
        RecursiveVerifyNode(((BinNode*)X)->_false, visit);   
    }
    else{ return; }
}
void CFA_impl::PrintCFA(){
    int i1;
    i1 = 0;
    set<Node*> visit;
    RecursiveVerifyNode(GetInitNode(), visit);
}
void CFA_impl::PrintBackNode(Node* n){
    int i1;
    i1 = 0;
    for(i1 = 0; i1 < (int)n->prev.size(); i1++){
        //if(typeid(*n) == typeid(UniNode)){ PrintProp(((UniNode*)n)->p); }
        if(n == NULL){ cout << "TermNode"; }
        else if(typeid(*n) == typeid(UniNode)){ PrintExpr(((UniNode*)n)->e1); cout << "="; PrintExpr(((UniNode*)n)->e2); }
        else if(typeid(*n) == typeid(BinNode)){ PrintProp(((BinNode*)n)->p); }
        else if(typeid(*n) == typeid(BadNode)){ cout << "BadNode" ; }
        else{ }
        cout << " -> ";
        //cout << n->prev[i1] << endl;
        //if(typeid(*(n->prev[i1])) == typeid(UniNode)){ PrintProp(((UniNode*)(n->prev[i1]))->p); }
        if(n->prev[i1] == NULL){ cout << "Terminal"; }
        else if(typeid(*(n->prev[i1])) == typeid(UniNode)){ 
            PrintExpr(((UniNode*)(n->prev[i1]))->e1); cout << "="; PrintExpr(((UniNode*)(n->prev[i1]))->e2);}
        else if(typeid(*(n->prev[i1])) == typeid(BinNode)){ PrintProp(((BinNode*)(n->prev[i1]))->p); }
        else if(typeid(*(n->prev[i1])) == typeid(BadNode)){ cout << "BadNode"; }
        else{ }
        cout << endl;
    }
}
void CFA_impl::RecursiveVerifyBackNode(Node* X, set<Node*> &visit){
    int i2;
    i2 = 0;
    if(visit.find(X) != visit.end()){ return; }
    PrintBackNode(X);
    visit.insert(X);
    for(i2 = 0; i2 < (int)X->prev.size(); i2++){
        RecursiveVerifyBackNode(X->prev[i2], visit);
    }
}
void CFA_impl::PrintBackCFA(){
    int i1;
    i1 = 0;
    set<Node*> visit;
    RecursiveVerifyBackNode(GetFinalNode(), visit);
}
void CFA_impl::BuildGraph(int i1){
    ProgramConnectType pct;
    map<Node*, char*> gotolist;
    Node* m;
    m = new BadNode;
    //cout << "size = " << fun.size() << " i1 = " << i1 << endl;
    //pct = BuildCFA_impl(*(fun[i1]), m, NULL, &gotolist);
    //pct = BuildCFA_impl(*prog1, m);
    ConnectGoto(&gotolist);
    SetInitNode(pct.init);
    //strcpy(id, fun[i1]->name);
    //formal_parameter = fun[i1]->formal_para;
    for(i1 = 0; i1 < (int)pct.ends1.size(); i1++){
        (*(pct.ends1[i1])) = NULL;
    }
}
void CFA_impl::GraphOPType(ofstream &out, OPType l){
    if(l == Plus){ out << "+"; }
    else if(l == Minus){ out << "-"; }
    else if(l == Multi){ out << "*"; }
    else if(l == Divide){ out << "/"; }
/*    else if(l == Bitor){ out << "|"; }
    else if(l == Bitand){ out << "&"; }
    else if(l == Bitxor){ out << "^"; }
    else if(l == Mod){ out << "mod"; }*/
    else{ }
}
void CFA_impl::GraphExpr(ofstream &out, Expr *e){
    if(typeid(*e) == typeid(IntExpr)){
        out << ((IntExpr*)e)->i;
    }
/*    else if(typeid(*e) == typeid(SelectExpr)){
        out << Expr2String(((SelectExpr*)e)->a) << "[";
        GraphExpr(out, e);
        out << "]";
    }*/
    else if(typeid(*e) == typeid(VarExpr)){
        out << ((VarExpr*)e)->x;
    }
    else if(typeid(*e) == typeid(BinExpr)){
        GraphExpr(out, ((BinExpr*)e)->e1);
        GraphOPType(out, ((BinExpr*)e)->op);
        GraphExpr(out, ((BinExpr*)e)->e2);
    }
    else{
        out << "error" << endl;
    }
}
void CFA_impl::GraphLogicType(ofstream &out, LogicType l){
    if(l == And){ out << "&&"; }
    else if(l == Or){ out << "||"; }
    else{ }
}
void CFA_impl::GraphPropType(ofstream &out, PropType l){
    if(l == LT){ out << "<"; }
    else if(l == GT){ out << ">"; }
    else if(l == Eq){ out << "=="; }
    else{ }
}
void CFA_impl::GraphProp(ofstream &out, Prop *p){
    if(typeid(*p) == typeid(BoolProp)){
        if(((BoolProp*)p)->b == true){ out << "TRUE"; }
        else{ out << "FALSE"; }
    }
    else if(typeid(*p) == typeid(NegProp)){
        out << "~(";
        GraphProp(out, ((NegProp*)p)->p);
	out<<")";
    }
    else if(typeid(*p) == typeid(BinProp)){
        GraphProp(out, ((BinProp*)p)->p1);
        GraphLogicType(out, ((BinProp*)p)->l);
        GraphProp(out, ((BinProp*)p)->p2);
    }
    else if(typeid(*p) == typeid(InequProp)){
        GraphExpr(out,((InequProp*)p)->e1);
        GraphPropType(out, ((InequProp*)p)->p);
        GraphExpr(out, ((InequProp*)p)->e2);
    }
    else{
        out << "error" << endl;
    }
}
void CFA_impl::GraphNodeUniNode(ofstream &out, Node* n){
    //{ st_Assign, st_Goto, st_Return, st_Label, st_FUNC_Call };
    out << "\"";
    if(((UniNode*)n)->e1 != NULL && ((UniNode*)n)->e2 != NULL){
        GraphExpr(out, ((UniNode*)n)->e1);
        out << "=";
        GraphExpr(out, ((UniNode*)n)->e2);
        if(((UniNode*)n)->st == st_FUNC_Call){
            out << "(";
            for(int i1 = 0; i1 < (int)((((UniNode*)n)->actualpara).size()); i1++){
                GraphExpr(out, (((UniNode*)n)->actualpara)[i1]);
                if(i1 != (int)((((UniNode*)n)->actualpara).size())-1){
                    out << ", ";
                }
            }
            out << ")";
        }
    }
    else if(((UniNode*)n)->e1 == NULL && ((UniNode*)n)->e2 != NULL){
        out << "\"" << "e1=NULL ERROR!!!";
    }
    else if(((UniNode*)n)->e1 != NULL && ((UniNode*)n)->e2 == NULL){
        if(((UniNode*)n)->st == st_Goto){
            out << "GOTO ";
            GraphExpr(out, ((UniNode*)n)->e1);
        }
        else if(((UniNode*)n)->st == st_Return){
            out << "RETURN ";
            GraphExpr(out, ((UniNode*)n)->e1);
        }
        else if(((UniNode*)n)->st == st_Label){
            GraphExpr(out, ((UniNode*)n)->e1);
            out << ":";
        }
    }
    else{
        out << "\"" << "e1=NULLe2=NULL ERROR!!!";
    }
    out << "(#" << n << ")" << "\"";
    return;
}
void CFA_impl::GraphNode(ofstream &out, Node* n, set<Node*> &visit){
    if(n == NULL){
        return;
    }
    else if(typeid(*n) == typeid(UniNode)){   
        //out << "\"" << ((UniNode*)n)->statement << "(#" << n << ")" << "\"";
        GraphNodeUniNode(out, n);
        if(((UniNode*)n)->next == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((UniNode*)n)->next)) == typeid(UniNode) ){
            out << " -> ";
            GraphNodeUniNode(out, ((UniNode*)n)->next);
            //out << "\"" << ((UniNode*)(((UniNode*)n)->next))->statement;
            //out << "(#" << ((UniNode*)n)->next << ")";
            //out << "\"";
        }
        else if(typeid(*((UniNode*)n)->next) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)(((UniNode*)n)->next))->p);
            out << "(#" << ((UniNode*)n)->next << ")";
            out << "\"";
        }
        else if(typeid(*((UniNode*)n)->next) == typeid(BadNode)){
            out << " -> \"BadNode\"";
        }
        else{
        }
        out << ";" << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_true == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((BinNode*)n)->_true)) == typeid(UniNode) ){
            out << " -> ";
            GraphNodeUniNode(out, ((BinNode*)n)->_true);
            //out << "\"" << ((UniNode*)(((BinNode*)n)->_true))->statement;
            //out << "(#" << ((BinNode*)n)->_true << ")";
            //out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_true)->p);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BadNode)){
            out << " -> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"Y\"]";
        out << ";" << endl;
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_false == NULL){
            out << "-> \"terminal\"";
        } 
        else if(typeid(*(((BinNode*)n)->_false)) == typeid(UniNode) ){
            out << " -> ";
            GraphNodeUniNode(out, ((BinNode*)n)->_false);
            //out << "\"" << ((UniNode*)(((BinNode*)n)->_false))->statement;
            //out << "(#" << ((BinNode*)n)->_false << ")";
            //out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_false)->p);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BadNode)){
            out << "-> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"N\"]";
        out << ";" << endl;
    }
    else{
    }
}
void CFA_impl::RecursiveGraphNode(ofstream& out, Node *X, set<Node*> &visit){
    if(visit.find(X) != visit.end()){ return; }
    visit.insert(X);
    GraphNode(out, X, visit);
    if(X == NULL){
        return;
    }
    else if(typeid(*X) == typeid(UniNode)){
        RecursiveGraphNode(out, ((UniNode*)X)->next, visit);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveGraphNode(out, ((BinNode*)X)->_true, visit);
        RecursiveGraphNode(out, ((BinNode*)X)->_false, visit);
    }
    else{
        return;
    }
}
void CFA_impl::PrintSingleNodeWithGraphviz(ofstream &out, Node* n){
    if(n == NULL){
        out << "\"TermNode\"";
    }
    else if(typeid(*n) == typeid(UniNode)){
        out << "\"" << ((UniNode*)n)->statement << "\"";
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\""; GraphProp(out, ((BinNode*)n)->p); out << "\"";
    }
    else if(typeid(*n) == typeid(BadNode)){
        out << "\"BadNode\"";
    }
    else{
    }
}
void CFA_impl::GraphNode1(ofstream &out, Node* n, set<Node*> &visit, int x, int y){
    if(typeid(*n) == typeid(UniNode)){
        out << "s" << visit.size() << "[shape=ellipse, label=";
        PrintSingleNodeWithGraphviz(out, ((UniNode*)n)->next);
        out << ", pos=\"" << x << "," << y-1 << "!\"];" << endl;
        out << "s" << visit.size()-1 << " -- s" << visit.size() << ";" << endl;
    }
    else if(typeid(*n) == typeid(BinNode)){
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_true == NULL){
            out << " -> \"terminal\"";
        }
        else if(typeid(*(((BinNode*)n)->_true)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"";
            //GraphProp(out, ((UniNode*)((BinNode*)n)->_true)->p);
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_true)->e1); out << "=";
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_true)->e2);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_true)->p);
            out << "(#" << ((BinNode*)n)->_true << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_true) == typeid(BadNode)){
            out << " -> \"BadNode\"";
        }
        else{
        }
        out << "[label = \"Y\"]";
        out << ";" << endl;
        out << "\"";
        GraphProp(out, ((BinNode*)n)->p);
        out << "(#" << n << ")";
        out << "\"";
        if(((BinNode*)n)->_false == NULL){
            cout << "-> \"terminal\"" << endl;
        } 
        else if(typeid(*(((BinNode*)n)->_false)) == typeid(UniNode) ){
            out << " -> ";
            out << "\"";
            //GraphProp(out, ((UniNode*)((BinNode*)n)->_false)->p);
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_false)->e1); out << "=";
            GraphExpr(out, ((UniNode*)((BinNode*)n)->_false)->e2);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BinNode)){
            out << " -> ";
            out << "\"";
            GraphProp(out, ((BinNode*)((BinNode*)n)->_false)->p);
            out << "(#" << ((BinNode*)n)->_false << ")";
            out << "\"";
        }
        else if(typeid(*((BinNode*)n)->_false) == typeid(BadNode)){
            cout << "-> \" BadNode\"" << endl;
        }
        else{
        }
        out << "[label = \"N\"]";
        out << ";" << endl;
    }
    else{
    }
}

void CFA_impl::RecursiveGraphNode1(ofstream& out, Node *X, set<Node*> &visit, int x, int y){
    if(visit.find(X) != visit.end()){ return; }
    visit.insert(X);
    GraphNode1(out, X, visit, x, y);
    if(typeid(*X) == typeid(UniNode)){
        RecursiveGraphNode1(out, ((UniNode*)X)->next, visit, x, y-1);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveGraphNode1(out, ((BinNode*)X)->_true, visit, x-6, y-1);
        RecursiveGraphNode1(out, ((BinNode*)X)->_false, visit, x+6, y-1);
    }
    else{
        return;
    }
}
void CFA_impl::CFA2Dot(const char *outputName){
    int i1;
    i1 = 0;
    ofstream out(outputName);
    set<Node*> visit;
    //out << "graph G {" << endl << "[overlap=false];" << endl;
    //out << "s0[label="; PrintSingleNodeWithGraphviz(out, GetInitNode()); out << ",pos=\"0.0,0.0!\"];" << endl;
    out << "digraph G {" << endl;
    RecursiveGraphNode(out, initNode, visit);
    //RecursiveGraphNode1(out, initNode, visit, 0, 0);
    out << "}";
}

 
void CFA_impl::setCFA(
vector<VarExpr*> i_formal_parameter,
map<Node*, char*> i_LabelSet,
Node* i_initNode,
string Name)
{
  formal_parameter = i_formal_parameter;
  LabelSet = i_LabelSet;
  initNode = i_initNode;
  //PrintCFA()
  //Name.append(".dot");
  //CFA2Dot(Name.c_str());
  return;
}


//refine ywlee CFA_impl
bool CFA_impl::CheckCFAValid(Node* node){
	return true;
}

void CFA_impl::RecursiveWalkNode(Node* X, set<Node*>& visit){
    if(visit.find(X) != visit.end()){ return; }
    //cout << "X = " << X << endl;
    visit.insert(X);
    if(X == NULL){ return;   }
    else if(typeid(*X) == typeid(UniNode)){ 
        RecursiveWalkNode(((UniNode*)X)->next, visit);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveWalkNode(((BinNode*)X)->_true, visit);
        RecursiveWalkNode(((BinNode*)X)->_false, visit);   
    }
    else{ return; }
}

void CFA_impl::RefineCFAywlee(){
    set<Node*> visit;
    RecursiveWalkNode(initNode, visit);
}
void CFA_impl::RecursiveVerifyNode(Node* X, set<Node*>& visit, vector<Expr*>& vv){
    if(visit.find(X) != visit.end()){ return; }
    //cout << "X = " << X << endl;
    //PrintNode(X);
    visit.insert(X);
    if(X == NULL){ return;   }
    else if(typeid(*X) == typeid(UniNode)){ 
        if(typeid(*(((UniNode*)X)->e1)) == typeid(VarExpr) ){
            if((strncmp(((VarExpr*)(((UniNode*)X)->e1))->x, "__CPROVER_", 10) != 0) && (strncmp(((VarExpr*)(((UniNode*)X)->e1))->x, "END_FUNCTION", 12) != 0)){
                //cout << "global = " << ((VarExpr*)(((UniNode*)X)->e1))->x << endl;
                vv.push_back(((UniNode*)X)->e1);
            }
        }
        RecursiveVerifyNode(((UniNode*)X)->next, visit, vv);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveVerifyNode(((BinNode*)X)->_true, visit, vv);
        RecursiveVerifyNode(((BinNode*)X)->_false, visit, vv);   
    }
    else{ return; }
}

void CFA_impl::GetGlobalVariable(vector<Expr*>& vv){
    set<Node*> visit;
    RecursiveVerifyNode(GetInitNode(), visit, vv);
}
void CFA_impl::RecursiveVerifyNode(Node* X, set<Node*>& visit, set<Node*> &vn){
    if(visit.find(X) != visit.end()){ return; }
    //cout << "X = " << X << endl;
    visit.insert(X);
    if(X == NULL){ return;   }
    else if(typeid(*X) == typeid(UniNode)){ 
        while( ((UniNode*)X)->next != NULL && typeid(*(((UniNode*)X)->next))==typeid(UniNode) && (((UniNode*)(((UniNode*)X)->next))->st == st_Label || ((UniNode*)(((UniNode*)X)->next))->st == st_Goto || ((UniNode*)(((UniNode*)X)->next))->st == st_None )){
            if(vn.find(((UniNode*)X)->next)!=vn.end()){ }
            else{ vn.insert(((UniNode*)X)->next); }
            if(((UniNode*)(((UniNode*)X)->next))->next != NULL){
                for(unsigned i1 = 0; i1 < (((UniNode*)(((UniNode*)X)->next))->next)->prev.size(); i1++){
                    if(((((UniNode*)(((UniNode*)X)->next))->next)->prev)[i1] == ((UniNode*)X)->next){
                        ((((UniNode*)(((UniNode*)X)->next))->next)->prev).erase(((((UniNode*)(((UniNode*)X)->next))->next)->prev).begin()+i1);
                        break;
                    }
                }
            }
            ((UniNode*)X)->next = ((UniNode*)(((UniNode*)X)->next))->next;
            if(((UniNode*)X)->next != NULL){
                (((UniNode*)X)->next)->prev.push_back(X);
            }
        }
        /*while( ((UniNode*)X)->next != NULL && typeid(*(((UniNode*)X)->next))==typeid(UniNode) && ((UniNode*)(((UniNode*)X)->next))->st == st_Goto){
            if(vn.find(((UniNode*)X)->next)!=vn.end()){ }
            else{ vn.insert(((UniNode*)X)->next); }
            ((UniNode*)X)->next = ((UniNode*)(((UniNode*)X)->next))->next;
            if(((UniNode*)X)->next != NULL){
                (((UniNode*)X)->next)->prev.push_back(X);
            }           
        }*/
        RecursiveVerifyNode(((UniNode*)X)->next, visit, vn);
    }
    else if(typeid(*X) == typeid(BinNode)){
        while( ((BinNode*)X)->_true != NULL && typeid(*(((BinNode*)X)->_true))==typeid(UniNode) && (((UniNode*)(((BinNode*)X)->_true))->st == st_Label || ((UniNode*)(((BinNode*)X)->_true))->st == st_Goto || ((UniNode*)(((BinNode*)X)->_true))->st == st_None)){
            if(vn.find(((BinNode*)X)->_true)!=vn.end()){ }
            else{ vn.insert(((BinNode*)X)->_true); }
            if(((UniNode*)(((BinNode*)X)->_true))->next != NULL){
                for(unsigned i1 = 0; i1 < (((UniNode*)(((BinNode*)X)->_true))->next)->prev.size(); i1++){
                    if(((((UniNode*)(((BinNode*)X)->_true))->next)->prev)[i1] == ((BinNode*)X)->_true){
                        ((((UniNode*)(((BinNode*)X)->_true))->next)->prev).erase(((((UniNode*)(((BinNode*)X)->_true))->next)->prev).begin()+i1);
                        break;
                    }
                }
            }
            ((BinNode*)X)->_true = ((UniNode*)(((BinNode*)X)->_true))->next;
            if(((BinNode*)X)->_true != NULL){
                (((BinNode*)X)->_true)->prev.push_back(X);
            }
        }
        RecursiveVerifyNode(((BinNode*)X)->_true, visit, vn);
        while( ((BinNode*)X)->_false != NULL && typeid(*(((BinNode*)X)->_false))==typeid(UniNode) && (((UniNode*)(((BinNode*)X)->_false))->st == st_Label || ((UniNode*)(((BinNode*)X)->_false))->st == st_Goto || ((UniNode*)(((BinNode*)X)->_false))->st == st_None)){
            if(vn.find(((BinNode*)X)->_false)!=vn.end()){ }
            else{ vn.insert(((BinNode*)X)->_false); }
            if(((UniNode*)(((BinNode*)X)->_false))->next != NULL){
                for(unsigned i1 = 0; i1 < (((UniNode*)(((BinNode*)X)->_false))->next)->prev.size(); i1++){
                    if(((((UniNode*)(((BinNode*)X)->_false))->next)->prev)[i1] == ((BinNode*)X)->_true){
                        ((((UniNode*)(((BinNode*)X)->_false))->next)->prev).erase(((((UniNode*)(((BinNode*)X)->_false))->next)->prev).begin()+i1);
                        break;
                    }
                }
            }

            ((BinNode*)X)->_false = ((UniNode*)(((BinNode*)X)->_false))->next;
            if(((BinNode*)X)->_false != NULL){
                (((BinNode*)X)->_false)->prev.push_back(X);
            }
        }
        RecursiveVerifyNode(((BinNode*)X)->_false, visit, vn);   
    }
    else{ return; }
}

void CFA_impl::LabelReduction(){
    set<Node*> visit;
    set<Node*> vn;
    while(GetInitNode() != NULL && typeid(*GetInitNode()) == typeid(UniNode) && ((UniNode*)(GetInitNode()))->st == st_Label){
        if(vn.find(GetInitNode())!=vn.end()){}
        else{ vn.insert(GetInitNode()); }
        (((UniNode*)(GetInitNode()))->next)->prev.clear();
        SetInitNode(((UniNode*)(GetInitNode()))->next);
    }
    while(GetInitNode() != NULL && typeid(*GetInitNode()) == typeid(UniNode) && ((UniNode*)(GetInitNode()))->st == st_Goto){
        if(vn.find(GetInitNode())!=vn.end()){}
        else{ vn.insert(GetInitNode()); }
        (((UniNode*)(GetInitNode()))->next)->prev.clear();
        SetInitNode(((UniNode*)(GetInitNode()))->next);
    }
    RecursiveVerifyNode(GetInitNode(), visit, vn);
    for(set<Node*>::iterator it = vn.begin(); it != vn.end(); it++){
        /*for(vector<Node*>::iterator it1 = (*it).prev.begin(); it1 != it->prev.end(); it1++){
            (((UniNode)(*it))->next)->prev.push_back(*it1);
        }*/
        delete *it;
    }
}
//void CFA_impl::RecursiveVerifyNode(Node* X, set<Node*>& visit, map<Node*, Node*> &not_information){
void CFA_impl::RecursiveVerifyNode(Node* X, set<Node*>& visit, vector<NotMidterm> &not_information){
    //cout << "X =" << X << endl;
    if(visit.find(X) != visit.end()){ return; }
    visit.insert(X);
    //std::map<Node*, Node*>::reverse_iterator not_it;
    //std::vector<NotMidterm>::reverse_iterator not_it;
    std::vector<NotMidterm>::iterator not_it;
    //for(not_it = not_replace.begin(); not_it != not_replace.end(); not_it++){
    //for(not_it = not_replace.rbegin(); not_it != not_replace.rend(); not_it++){
    //for(not_it = not_replace.rbegin(); not_it != not_replace.rend(); not_it++){
    for(not_it = not_replace.begin(); not_it != not_replace.end(); not_it++){
        if(not_it->second == X){
            for(unsigned i1 = 0; i1 < X->prev.size(); i1++){
//cout << " ============= " << i1 << " " << X->prev.size() << X->prev[i1] << " " << X << endl;
//PrintNode((X->prev[i1]));
                if(typeid(*((X->prev)[i1])) == typeid(UniNode)){
                    ((UniNode*)((X->prev)[i1]))->next = not_it->first;
                    (not_it->first)->prev.push_back((X->prev)[i1]);
                }
                else if(typeid(*((X->prev)[i1])) == typeid(BinNode)){
                    if(((BinNode*)((X->prev)[i1]))->_true == X){
                        ((BinNode*)((X->prev)[i1]))->_true = not_it->first;
                        (not_it->first)->prev.push_back((X->prev)[i1]);
                    }
                    else if(((BinNode*)((X->prev)[i1]))->_false == X){
                        ((BinNode*)((X->prev)[i1]))->_false = not_it->first;
                        (not_it->first)->prev.push_back((X->prev)[i1]);
                    }
                    else{
                        cout << "NOT ERROR!!!1" << endl; 
                    }
                }
                else{
                    cout << "NOT ERROR!!!2" << endl; 
                }
            }//top change to another graph
            X->prev.clear();
            ((UniNode*)(((BinNode*)(not_it->first))->_true))->next = X;
            ((UniNode*)(((BinNode*)(not_it->first))->_false))->next = X;
            X->prev.push_back(((BinNode*)(not_it->first))->_true);
            X->prev.push_back(((BinNode*)(not_it->first))->_false);
            /*cout << "first =>" << not_it->first << " present node =>" << X << endl;
            PrintNode(not_it->first);
            cout << "second => " << not_it->second << " present node =>" << X << endl;
            PrintNode(not_it->second);*/
        }
    }
    if(X == NULL){ return;   }
    else if(typeid(*X) == typeid(UniNode)){ 
        RecursiveVerifyNode(((UniNode*)X)->next, visit, not_information);
    }
    else if(typeid(*X) == typeid(BinNode)){
        RecursiveVerifyNode(((BinNode*)X)->_true, visit, not_information);
        RecursiveVerifyNode(((BinNode*)X)->_false, visit, not_information);   
    }
    else{ return; }
}

void CFA_impl::NotReplace(){
    set<Node*> visit;
    //std::map<Node*, Node*>::iterator not_it;
    //for(not_it = not_replace.begin(); not_it != not_replace.end(); not_it++){
    //std::map<Node*, Node*>::reverse_iterator not_it;
    //std::vector<NotMidterm>::reverse_iterator not_it;
    std::vector<NotMidterm>::iterator not_it;
    //for(not_it = not_replace.rbegin(); not_it != not_replace.rend(); not_it++){
    //for(not_it = not_replace.rbegin(); not_it != not_replace.rend(); not_it++){
    for(not_it = not_replace.begin(); not_it != not_replace.end(); not_it++){
        //PrintNode(not_it->first);
        if(not_it->second == GetInitNode()){
            ((UniNode*)(((BinNode*)(not_it->first))->_true))->next = GetInitNode();
            ((UniNode*)(((BinNode*)(not_it->first))->_false))->next = GetInitNode();
            GetInitNode()->prev.push_back(((BinNode*)(not_it->first))->_true);
            GetInitNode()->prev.push_back(((BinNode*)(not_it->first))->_false);
            SetInitNode(not_it->first);
        }
    }
    RecursiveVerifyNode(GetInitNode(), visit, not_replace);
}
